Section: New Results

Weak Memory Models, Litmus-PPC-WMM tools

Participants : Jade Alglave, Luc Maranget, Pankaj Pawan, Susmit Sarkar [U. of Cambridge] , Peter Sewell [U. of Cambridge] , Francesco Zappa Nardelli.

Shared memory multiprocessors typically expose subtle, poorly understood and poorly specified relaxed-memory semantics to programmers. To understand them, and to develop formal models to use in program verification, we find it essential to take an empirical approach, testing what results parallel programs can actually produce when executed on the hardware. We describe a key ingredient of our approach, our litmus tool, which takes small “litmus test” programs and runs them for many iterations to find interesting behaviour. It embodies various techniques for making such interesting behaviour appear more frequently. We presented a tool, litmus, to run “litmus tests”. on real hardware at TACAS'11 [31] .

An automated exploration of machine memory models (on the dont tool) is submitted to TACAS'12.

During a two month long intership, Pankaj Pawan (IIT Kanpur, India) ported the PPCMEM application from OCaml to JavaScript, and developed a suitable web-interface. This enabled a wide dissemination (including at IBM) of the PPCMEM tool. The tool is available online at: http://www.cl.cam.ac.uk/~pes20/ppcmem/help.html .